| Definitions |  b, {x:A| B(x)} , E(X), t  T, s = t, x:A  B(x),  x:A. B(x), E, a:A fp B(a), strong-subtype(A;B), P   Q, ES, AbsInterface(A), Type, x:A  B(x), left + right, let x,y = A in B(x;y), t.1, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , chain_config(), chain_sys(Cmd), e  X, X(e), Id, type List, valid-sys(es;Config;Sys;e), EState(T), f(a),  , EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M),  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e',  , constant_function(f;A;B), SWellFounded(R(x;y)),  , pred!(e;e'),   x,y. t(x;y), <a, b>,  A, pred(e), first(e), x. t(x), P & Q, Top, Void, False, P  Q, Dec(P), P  Q, a < b, A B,  x:A. B(x), b | a, a ~ b, a b, a <p b, a < b, A c B, x f y, xL. P(x), (xL.P(x)), r < s, q-rel(r;x), Outcome, (x l), l_disjoint(T;l1;l2), (e <loc e'), e loc e' , (e < e'), e c e', e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), x dom(f),  x:A.B(x), inr x , "$token", ccpred?(x), inl x , Atom, x.A(x), ccpred-id(x), ccsucc?(x), cctail?(x), cchead?(x), Atom$n, loc(e), ff, tt, True, a = b, P Q, locl(a), e@i. P(e), x(s), MaName, chain sys ind csupdate compseq tag def, chain_sys_ind(x;cmd.input(cmd);from,cmds.update(from;cmds)), csupdate(from;cmds), chain sys ind csinput compseq tag def, csinput(cmd), {T} |
| Lemmas | chain sys-induction, pi1 wf, chain sys ind wf, csinput wf, decidable or, csupdate wf, decidable existse-before, decidable equal Id, decidable alle-lt, es-causl wf, iff wf, rev implies wf, assert-eq-id, decidable implies better, decidable es-locl, decidable not, es-is-interface wf, true wf, btrue wf, bfalse wf, es-loc wf, decidable cand, cchead? wf, cctail? wf, ccsucc? wf, existse-before wf, ccpred-id wf, alle-lt wf, es-locl wf, ccpred? wf, chain config wf, decidable assert, decidable wf, false wf, valid-sys wf, event system wf, deq wf, EOrderAxioms wf, IdLnk wf, Msg wf, unit wf, nat wf, val-axiom wf, qle wf, cless wf, bool wf, top wf, Knd wf, kindcase wf, constant function wf, not wf, loc wf, pred! wf, strongwellfounded wf, rationals wf, EState wf, es-interface-val wf, Id wf, es-interface wf, chain sys wf, es-interface-val wf2, member wf, es-E-interface wf, es-E wf, subtype rel wf, assert wf |